/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305

␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 	ISeptember 18, 1980 




␈↓ ↓H␈↓Professor Fred Abramson
␈↓ ↓H␈↓Department of Mathematics
␈↓ ↓H␈↓University of Notre Dame
␈↓ ↓H␈↓Notre Dame, INDIANA 46556

␈↓ ↓H␈↓Dear Professor Abramson:

␈↓ ↓H␈↓        Many␈αthanks␈α
for␈αyour␈αletter␈α
of␈αSeptember␈α
11,␈αwhich␈αI␈α
have␈αdiscussed␈α
it␈αwith␈αJussi␈α
Ketonen.
␈↓ ↓H␈↓There␈αare␈α
two␈αpossibilities␈α
and␈αyou␈α
might␈αbe␈αinterested␈α
in␈αboth.␈α
 One␈αis␈α
to␈αwork␈α
with␈αJussi␈αon␈α
his
␈↓ ↓H␈↓new␈α∩interactive␈α∩theorem␈α⊃prover,␈α∩and␈α∩he␈α∩can␈α⊃explain␈α∩to␈α∩you␈α∩what␈α⊃is␈α∩involved␈α∩in␈α∩detail,␈α⊃but
␈↓ ↓H␈↓basically␈αit␈αis␈αprogramming␈αinference␈α
procedures␈αand␈αproof-≡nding␈αprocedures␈αin␈α
Maclisp,␈αwhich
␈↓ ↓H␈↓he␈αsuggests␈αyou␈αlearn␈αin␈αadvance␈αof␈αcoming.␈α The␈αother␈αis␈αto␈αwork␈αon␈αformalizing␈αcommon␈αsense
␈↓ ↓H␈↓facts about the world in logic, which is my main activity.

␈↓ ↓H␈↓        At␈α
the␈α
moment␈αI␈α
don't␈α
have␈α
the␈αmoney␈α
to␈α
support␈αyou,␈α
but␈α
there␈α
is␈αa␈α
good␈α
chance␈αthat␈α
good
␈↓ ↓H␈↓news␈αwill␈αarrive␈αin␈αJanuary.␈α If␈αyou␈αcan␈αget␈αthe␈αmoney␈αfrom␈αelsewhere,␈αyou␈αare␈αcertainly␈αwelcome
␈↓ ↓H␈↓to use our facilities to take part in our activities.


␈↓ ↓H␈↓Best regards,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science

␈↓ ↓H␈↓cc: Jussi Ketonen